\begin{tabbing}
$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]($\forall$$x$:$T$. $\neg$$R$($x$,$x$))
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:$T$. $R$($x$,$y$) $\Rightarrow$ $\neg$$R$($y$,$x$))
\\[0ex]$\Rightarrow$ (\=$\forall$${\it as}$, ${\it bs}$:$T$ List.\+
\\[0ex]l{-}ordered($T$;$x$,$y$.$R$($x$,$y$);${\it as}$)
\\[0ex]$\Rightarrow$ l{-}ordered($T$;$x$,$y$.$R$($x$,$y$);${\it bs}$)
\\[0ex]$\Rightarrow$ (${\it as}$ $=$ ${\it bs}$ $\Leftrightarrow$ ($\forall$$x$:$T$. ($x$ $\in$ ${\it as}$) $\Leftrightarrow$ ($x$ $\in$ ${\it bs}$))))
\-
\end{tabbing}